I think the structure is mostly ok, but please check my comments. This PR is missing tests though. Please add a few to folder src/test/resources/regressions/features/refute (which needs to be created). We usually write multiple types of tests:

• type-checking tests, e.g., what happens when we write refute 1? Does Gobra provide an error in the correct line?
• successful verification tests, i.e., tests that use the feature and should succeed.
• failed verification tests - these should indicate what is the expected verification error.

To annotate the expected type errors and verification errors, we use an annotation system that is exemplified in https://github.com/viperproject/gobra/tree/master/src/test/resources/regressions/features/opaque. Essentially, we use //:: ExpectedOutput(type_error) in the line before the expected type error and //:: ExpectedOutput(error:cause) before the line where a verification error is expected, where error and cause are replaced by the ids of the error kind and cause that you added

LGTM! I just have a few small nitpicks, please address them before merging. Please use the option "Squash and merge" when merging this in master (on the Github CLI).

For future reference, this PR has more cool things besides refute:

• It refactors Gobra to use the FrontendAPI, which besides other things, gives us pretty-printed Viper code that is easier to read e.g., it shows the code prior to applying the termination plugin. (This has the side effect of pretty-printing ill-formed Viper code due to a bug in silver where decreases clauses are printed as requires decreases ..., but that is a bug that we need to fix in silver anyway)
• It fixes the error reporting in verification errors related to closures
• It deprecates part of the TerminationTransformer (we might be able to drop this entirely in the future)